T:Type, L:(T List), n:{0..(||L||+1)}, x:T. (x  firstn(n;L))  (i:{0..n}. (x = L[i])) 

latex

Definitions

x:A. B(x), ||as||, firstn(n;as), Y, t  T, {i..j}, P  Q, (x  l), x:A. B(x), , A c B, P & Q, P  Q, P  Q, A  B, i  j < k, A, False, , if b then t else f fi , tt, ff, T, True, P  Q, l[i], hd(l), nth_tl(n;as), i z j, b, i <z j, {T}, , Unit, Dec(P),

Lemmas

le wf, select wf, length wf2, nat wf, int seg wf, lt int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of lt int, le int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, length wf1, iff functionality wrt iff, l member wf, firstn wf, length cons, non neg length, cons member, select cons tl, decidable lt, select cons hd, decidable false, nil member